The main goal in this paper is to use a dual equivalence in automata theory started in [25] and developed in [3] to prove a general version of the Eilenberg-type theorem presented in [4]. Our principal results confirm the existence of a bijective correspondence between three concepts; formations of monoids, formations of languages and formations of congruences. The result does not require finiteness on monoids, nor regularity on languages nor finite index conditions on congruences. We relate our work to other results in the field and we include applications to non-r-disjunctive languages, Reiterman s equational description of pseudovarieties and varieties of monoids. ; The authors gratefully acknowledge various discussions with Jean-Eric Pin. This work has been supported by the grants MTM2010-19938-C03-01 from the Ministerio de Ciencia e Innovacion (Spanish Government) and MTM2014-54707-C3-1-P from the Ministerio de Economia y Competitividad (Spanish Government) and FEDER (European Union). The first author has been supported by the grant No. 11271085 from the National Natural Science Foundation of China. The second author has been supported by the predoctoral grant AP2010-2764 from the Ministeriode Educacion (Spanish Government) and by an internship from CWI. ; Ballester Bolinches, A.; Cosme-Llópez, E.; Esteban Romero, R.; Rutten, J. (2015). Formations of monoids, congruences, and formal languages. Scientific Annals of Computer Science. 25(2):171-209. https://doi.org/10.7561/SACS.2015.2.171 ; S ; 171 ; 209 ; 25 ; 2
Formal languages are sequences of symbols in some discrete set called alphabet. They are often specified by formulas in some logic, by rational expressions or else by discrete automata of various types. Current theory is mostly qualitative, in the sense that its objects are sequences over a discrete, non-metric, time, that acceptation of a sequence over an automaton depends on whether an accepting state is visited or not, and that, for language comparison, one will most often consider inclusion than quantitative measures. This thesis contributes to the study of these often neglected aspects by presenting fundamental results in three new quantitative problem classes about formal languages. In the first chapter, we study a class of scheduling problems which combines structural aspects related to dependencies between tasks with dynamical aspects of online scheduling. We show that some task request streams in this class of problems, however admissible in the sense that they do not require more raw resource utilization than available machines can provide, cannot be scheduled with bounded latency. However, we develop a scheduling policy which can guarantee a bounded backlog accumulation for all admissible streams even without knowledge of the stream content prior to execution. We show that if the streams actually are sub-critical, then the same policy also guarantees a bounded latency. In quantitative verification, states and transitions of a system can be endowed with costs, which can be used to associate average costs to infinite behaviors. In this second part, we propose to define omega-languages thanks to Boolean queries concerning average costs. Specifications dealing with averages, such as "average message loss is under some threshold" are not omega-regular, but can be expressed in our model. Hence we study expressive power and Borel complexity of such specifications. We show that in order to ensure closure by intersection, multi-dimensional costs have to be considered. In the general case, we show that accepting conditions can be defined on the set of accumulation points of the sequence of the average costs of the prefixes of a run. We accurately characterize such sets. Last, we also propose a class of multi-threshold mean-payoff languages, in which extremal values of coordinates of points of the accumulation set are compared to constants. We show this class is closed under Boolean operations and analyzable. In the last chapter, we define two measures for a timed language: the volume of its sub-languages of words having a fixed number of discrete events, and entropy, which is the asymptotic logarithmic growth of volumes. These measures can be used to compare languages quantitatively and entropy can be seen as information content of a typical event of a typical word of in a language. For languages accepted by deterministic timed automata, we give an exact formula for the volume. Next we characterize entropy, thanks to functional analysis techniques, as the logarithm of the spectral radius of some positive integral operator. We give several methods to compute entropy: a symbolical one for the special case of "one clock and a half" automata, and two numerical ones: one using functional analysis, the other using discretization techniques. Last we establish an interpretation of this entropy in information theory by showing its relation with Kolmogorov complexity. ; Les langages formels sont des séquences sur un ensemble discret de symboles appelé alphabet. On les spécifie souvent par des formules dans une certaine logique, par des expressions rationnelles ou bien par des automates discrets de types variés. La théorie actuelle est principalement qualitative, dans le sens où ses objets sont des séquence sur un temps discret, non-métrique, dans le sens où l'acceptation d'une séquence sur un automate dépend du fait que l'on visite ou non un état accepteur, et enfin dans le sens où la comparaison de langages est plus souvent considérée en termes d'inclusion, plutôt qu'en termes de mesures quantitatives. Cette thèse contribue à l'étude de ces aspects souvent négligés en présentant des résultats fondamentaux dans trois nouvelles classes de problèmes quantitatifs sur les langages formels. Dans la première partie, nous étudions une classe de problèmes d'ordonnancement qui combine les aspects structurels associés aux dépendances entre tâches avec les aspects dynamiques liés au fait qu'un flux de requêtes arrive en continu pendant l'exécution. Nous montrons que, dans cette classe de problèmes, certains flux, pourtant admissibles dans le sens que les requêtes ne représentent pas plus de travail que ce que les machines peuvent traiter, ne peuvent pas être ordonnancé avec une latence bornée. Cependant nous développons une politique d'ordonnancement que peut garantir une accumulation de retard bornée pour tout flux de requêtes admissible, même sans le connaître à l'avance. Nous montrons que si les flux sont sous-critiques, alors cette même politique peut garantir une latence bornée. En vérification quantitative, les états et transitions d'un système peuvent être associés à des coûts, et ceux-ci utilisés pour associer des coûts moyens aux comportements infinis. Dans cette seconde partie, nous proposons de définir des omega-langages par des requêtes booléennes sur les coûts moyens. Des spécifications concernant des moyennes, tels que " le taux de perte moyen de messages est inférieur à un certain seuil " ne sont pas omega-régulières, mais exprimables dans notre modèle. Ainsi, nous étudions l'expressivité et la complexité de Borel de telles spécifications. Nous montrons que pour la clôture par intersection, il est nécessaire de considérer des coûts multi-dimensionnels. Nous mettons en évidence que dans le cas général, les conditions d'acceptation portent sur l'ensemble des points d'accumulation de la séquence des coûts moyens des préfixes d'une exécution, et nous donnons une caractérisation précise de tels ensembles. Nous proposons une classe de langages de coût moyen à seuils multiples, comparant les coordonnées minimales et minimales des points de cet ensemble à des constantes. Nous montrons enfin que cette classe est close par opérations booléennes et analysable. Enfin, dans le dernier volet, nous définissons deux mesures pour un langage temporisé : le volume de ses sous-langages de mots à nombre d'événements fixe et l'entropie (vitesse de croissance), mesure asymptotique pour un nombre non borné d'événements. Ces mesures peuvent être utilisées pour la comparaison quantitative de langages, et l'entropie peut être vue comme la quantité d'information par événement dans un mot typique du langage temporisé. Pour les langages acceptés par des automates temporisés déterministes, nous donnons une formule exacte pour le volume. Ensuite, nous caractérisons l'entropie, en utilisant des méthodes d'analyse fonctionnelle, en tant que logarithme du rayon spectral d'un opérateur intégral positif. Nous établissons plusieurs méthodes pour calculer l'entropie : une symbolique pour les automates que nos appelons " à une horloge et demie ", et deux numériques : une utilisant les techniques d'analyse fonctionnelle, l'autre basée sur la discrétisation. Nous donnons une interprétation de l'entropie en théorie de l'information en termes de complexité de Kolmogorov.
Während des Fabriklebenszyklus werden viele verschiedene Simulationsmodelle eingesetzt. Diese benötigen spezialisierte Simulationsmethoden und -werkzeuge, die je ein neues Simulationsmodell erfordern, das manuell in einer spezifischen Modellierungssprache erstellt wird. Der Beitrag zeigt eine Analyse von Ansätzen für die Fabriksimulationsbeschreibung mit dem Ziel einer durchgängigen Fabriksimulation. Diese erlauben einen Datenaustausch, aber keine dynamische Kopplung oder Generierung, darum wird ein Fabrikmodell umrissen. A wide variety of simulation models are used during the factory lifecycle. They require many specialized simulation methods and tools each requiring a new simulation model which is manually created in a specific modeling language. This paper shows an analysis of existing approaches and data models for factory simulation description with the goal of a consistent factory simulation. These allow data exchange, but not dynamic coupling or model generation, therefore a factory model is outlined.
Abstract This article explores 'smart contracts' from first principles: What they are, whether they are properly called 'contracts', and what issues they raise for national contract law. A 'smart' contract purports to record contractual promises in language which is both intelligible to human beings and (ultimately) executable by machines. The formalisation of contracting language that this entails is, I argue, the most important aspect for lawyers—just as important as the automation of contractual performance. Rather than taking a doctrinal approach focused on the presence of traditional indicia of contract formation, I examine the nature of contracts as legal entities created by words and documents. In most cases, smart contracts will be 'wrapped in paper' and nested in a national legal system. Borrowing from the idiom of computer science, I introduce the term 'contract stack' to highlight the complex nature of contracts as legal entities incorporating different 'layers', including speech acts by the parties in both natural and formal languages as well as mandatory legal rules. It is the interactions within this contract stack that will be most important to the development of contract law doctrines appropriate to smart contracts. To illustrate my points, I explore a few issues that smart contracts might raise for English contract law. I touch on the questions of illegality, jurisdiction, and evidence, but my focus in this paper is on exploring issues in contract law proper. This contribution should be helpful not only to lawyers attempting to understand smart contracts, but to those involved in coding smart contracts—and writing the languages used to code them.
The research work disclosed in this publication is partially funded by the Strategic Educational Pathways Scholarship Scheme (Malta). The scholarship is part financed by the European Union European Social Fund. ; The use of behavioural contracts, to specify, regulate and verify systems, is particularly relevant to runtime monitoring of distributed systems. System distribution poses major challenges to contract monitoring, from monitoring-induced information leaks to computation load balancing, communication overheads and fault-tolerance. We present mDPi, a location-aware process calculus, for reasoning about monitoring of distributed systems. We define a family of Labelled Transition Systems for this calculus, which allow formal reasoning about di erent monitoring strategies at di erent levels of abstractions. We also illustrate the expressivity of the calculus by showing how contracts in a simple contract language can be synthesised into di erent mDPi monitors. ; peer-reviewed
Argues that source studies need further development in Russian linguistics since involving a wider range of manuscripts into investigation may answer many questions that are actually faced by the historical lexicology and lexicography. It may also help to reconstruct the historical language development in detail. This approach is particularly relevant in the studies of the Russian language of the 18th century. While it is mainly based on the published texts, there is a lot of manuscripts that have not been studied yet but may greatly contribute to understanding of both the formal language developments and emergence of a new type of literary Russian language or the language of Russian nation. The special emphasis is to be put on research of the regional manuscripts which are also important for studying the formal language as they represent its local variations and local vocabulary which cannot be found in the records of the central institutions. The main issues of linguistic study stated above are considered on the example of the North Russian manuscripts of the early 18th century, namely the customs books of Kevrola, a town in the Archangel region.
